Language/OS - Multiplatform Resource Library

home *** CD-ROM | disk | FTP | other *** search

/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / ast_comp / concurre.tar / concurrency / ABSTRACTS next >

Wrap

Text File | 1993-07-05 | 26.2 KB | 600 lines

Papers on Foundations of Concurrency Available by Anonymous FTP from Boole.Stanford.EDU This file is ABSTRACTS in the /pub directory of Boole.Stanford.EDU, 36.8.0.65, accessible by anonymous ftp. The /pub directory is for FTP distribution of prepublications in the area of foundations of concurrency. It is run by the Boole group, a subgroup of the Mathematical Theory of Computation group, Computer Science Department, Stanford University. The group consists of the following people. Gidi Avrahami gidi@cs.stanford.edu (SYS) Carolyn Brown cbrown@cs.stanford.edu Rob van Glabbeek rvg@cs.stanford.edu Jeremy Gunawardena jhcg@cs.stanford.edu Vineet Gupta vgupta@cs.stanford.edu David Magerman magerman@cs.stanford.edu Vaughan Pratt (group leader) pratt@cs.stanford.edu (SYS) Marianne Siroker (secretary) siroker@cs.stanford.edu ==========================Instructions================================= FTP LOGIN. Give the following commands. ftp boole.stanford.edu Login: anonymous (if you don't have an account on boole) Paswd: user@host (your usual email address) bin (if you are retrieving a .dvi file) prompt off (if you want no ? prompts from mget) ls -ltr (see what's there, most recent last) mget filename-1 ... filename-n (e.g. mget cg.tex es.tex dti.tex) quit (exit from FTP) SOURCE. To retrieve the source to paper foo, get foo.tex. The source should be compiled using latex foo twice, the second time being to resolve cross-references (if this annoys you let lamport@src.dec.com know). A third time may be necessary with particularly complex documents, e.g. theses. DVI. If you wish to print paper foo without having to compile with latex, first "cd DVI" then retrieve foo.dvi. You must previously have given the "bin" command to ftp since .dvi files are not text files. Print foo.dvi on your host using lpr -d foo.dvi We are considering not storing .dvi files in future. If this would inconvenience you, please let us know to what extent. We make every effort to avoid nonstandard macros and fonts. PROBLEMS. If you have problems in either retrieving or compiling papers, please contact a systems person (flagged SYS on the list above). ===========================Available papers================================= TITLES scbr.tex The Second Calculus of Binary Relations spectrum.ps The linear time - branching time spectrum II complete.tex A complete ax'n for branching bisim. cong. of fin.state behaviours. ql.tex Linear Logic for Generalized Quantum Mechanics dti.tex The Duality of Time and Information ldomain.tex Disjunctive Systems and L-Domains monoidal.tex Some Monoidal Closed Categories of Stable Domains & Event Struct's 2d.tex A Roadmap of Some Two-Dimensional Logics ocbr.tex Origins of the Calculus of Binary Relations dalg.tex Dynamic Algebras: Examples, Constructions, Applications algecon.tex Arithmetic + Logic + Geometry = Concurrency esrs.tex Event Spaces and Related Structures crewthes.tex Metric Process Models atch.tex Interleaving Semantics and Action Refinement with Atomic Choice casthes.tex On the Specification of Concurrent Systems es.tex Event Spaces and their Linear Logic cg.tex Modeling Concurrency with Geometry jelia.tex Action Logic and Pure Induction man.tex Temporal Structures pp2.tex Teams Can See Pomsets am4.tex Enriched Categories and the Floyd-Warshall Connection iowatr.tex Dynamic Algebras as a well-behaved fragment of Relation Algebras ijpp.tex Modelling Concurrency with Partial Orders ----------------------------------------------------------------------- ABSTRACTS scbr.tex @InProceedings( Pr93b, Author="Pratt, V.R.", Title="The Second Calculus of Binary Relations", Booktitle="MFCS'93, Gda{\'{n}}sk", Address="Poland", Year=1993) We view the Chu space interpretation of linear logic as an alternative interpretation of the language of the Peirce calculus of binary relations. Chu spaces amount to K-valued binary relations, which for K=2^n we show generalize n-ary relational structures. We also exhibit a four-stage unique factorization system for Chu transforms that illuminates their operation. spectrum.ps.Z spectrum.A4.ps.Z @techreport{ vG92, author= "R.J. van Glabbeek", title = "The linear time -- branching time spectrum II; the semantics of sequential systems with silent moves", address = Stanford, year = 1993, note = "Available by anonymous ftp from Boole.stanford.edu"} This paper studies semantic equivalences and preorders for sequential systems with silent moves, restricting attention to the ones that abstract from successful termination, stochastic and real-time aspects of the investigated systems, and the structure of the visible actions systems can perform. It provides a parameterized definition of a such a preorder, such that most such preorders and equivalences found in the literature are obtained by a suitable instantiation of the parameters. Other instantiations yield preorders that combine properties from various semantics. Moreover, the approach shows several ways in which preorders that were originally only considered for systems without silent moves, most notably the ready simulation, can be generalized to an abstract setting. All preorders come with---or rather as---a modal characterization, and when possible also a relational characterization. Moreover they are motivated by means of an (also parameterized) testing scenario, phrased in terms of `button pushing experiments' on generative and reactive machines. The testing scenarios for branching bisimulation, eta-bisimulation and coupled simulation and the corresponding modal characterizations are especially new. complete.tex @TechReport( vG92, Author="R.J. van Glabbeek", Title ="A complete axiomatization for branching bisimulation congruence of finite-state behaviours", Address=Stanford, Note="Available by anonymous ftp from Boole.stanford.edu", Year=1992) This paper offers a complete inference system for branching bisimulation congruence on a basic sublanguage of CCS for representing regular processes with silent moves. Moreover, complete axiomatizations are provided for the guarded expressions in this language, representing the divergence- free processes, and for the recursion-free expressions, representing the finite processes. Furthermore it is argued that in abstract interleaving semantics (at least for finite processes) branching bisimulation congruence is the finest reasonable congruence possible. ql.tex @InProceedings( Pr93a, Author="Pratt, V.R.", Title="Linear Logic for Generalized Quantum Mechanics", Booktitle="Proc. Workshop on Physics and Computation (PhysComp'92)", Address="Dallas", Publisher="{IEEE}", Year=1993) Quantum logic is static, describing automata having uncertain states but no state transitions and no Heisenberg uncertainty tradeoff. We cast Girard's linear logic in the role of a dynamic quantum logic, regarded as an extension of quantum logic with time nonstandardly interpreted over a domain of linear automata and their dual linear schedules. In this extension the uncertainty tradeoff emerges via the ``structure veil.'' When VLSI shrinks to where quantum effects are felt, their computer-aided design systems may benefit from such logics of computational behavior having a strong connection to quantum mechanics. dti.tex @InProceedings( Pr92e, Author="Pratt, V.R.", Title="The Duality of Time and Information", Booktitle="Proc. of CONCUR'92", Pages="?-?+16", Publisher="Springer-Verlag", Address="Stonybrook, New York", Month=Aug, Year=1992) The states of a computing system bear information and change time, while its events bear time and change information. We develop a primitive algebraic model of this duality of time and information for rigid local computation, or straightline code, in the absence of choice and concurrency, where time and information are linearly ordered. This shows the duality of computation to be more fundamental than the logic of computation for which choice is disjunction and concurrency conjunction. To accommodate flexible distributed computing systems we then bring in choice and concurrency and pass to partially ordered time and information, the formal basis for this extension being Birkhoff-Stone dualtiy. A degree of freedom in how this is done permits a perfectly symmetric logic of computation amounting to Girard's full linear logic, which we view as the natural logic of computation when equal importance is attached to choice and concurrency. We conclude with an assessment of the prospects for extending the duality to other organizations of time and information besides partial orders in order to accommodate real time, nonmonotonic logic, and automata that can forget, and speculate on the philosophical significance of the duality. monoidal.tex @Article( Zh92a, Author="Zhang, Guo-Qiang", Title="Some Monoidal Closed Categories of Stable Domains and Event Structures", Journal="Mathematical Structures in Computer Science", Year=1992(to appear)) This paper introduces the following new constructions on stable domains and event structures: the tensor product, the linear function space, and the exponential. It results in a monoidal closed category of dI-domains as well as one of stable event structures which can be used to interpret intuitionistic linear logic. Finally, the usefulness of the category of stable event structures for modeling concurrency and its relation to other models is discussed. ldomain.tex @InProceedings( Zh92b, Author="Zhang, Guo-Qiang", Title="Disjunctive Systems and L-Domains", Booktitle="International Colloquium on Automata, Languages, and Programming", Address="Wien, Austria", Year=1992) Disjunctive systems are a representation of L-domains. They use sequents of the form X|-Y, with X finite and Y pairwise disjoint. We show that for any disjunctive system, its elements ordered by inclusion form an L-domain. On the other hand, via the notion of stable neighborhoods, every L-domain can be represented as a disjunctive system. More generally, we have a categorical equivalence between the category of disjunctive systems and the category of L-domains. A natural classification of domains is obtained in terms of the style of the entailment: when |X| = 2 and |Y| = 0, disjunctive systems determine coherent spaces; when |Y| <= 1 they represent Scott domains; when either |X| = 1 or |Y| = 0 the associated cpos are distributive Scott domains; and finally, without any restriction, disjunctive systems give rise to L-domains. 2d.tex @InProceedings( Pr92c, Author="Pratt, V.R.", Title="A Roadmap of Some Two-Dimensional Logics", Booktitle="Proc. of Workshop on Logic and the Flow of Information", Address="Amsterdam", Year=1992) We define the notion of two-dimensional logic and diagram the relative locations of a number of such. ocbr.tex @InProceedings( Pr92b, Author="Pratt, V.R.", Title="Origins of the Calculus of Binary Relations", Booktitle="Proc. 7th Annual IEEE Symp. on Logic in Computer Science", Address="Santa Cruz, CA", Month=Jun, Year=1992) The calculus of binary relations was introduced by De Morgan in 1860, and was subsequently greatly developed by Peirce and Schroeder. Half a century later Tarski, J'onsson, Lyndon, and Monk further developed the calculus from the perspective of modern model theory. dalg.tex @Article( Pr92d, Author="Pratt, V.R.", Title="Dynamic Algebras: Examples, Constructions, Applications", Journal="Studia Logica", Year=1992) Dynamic algebras combine the classes of Boolean (B + ' 0) and regular (R U ; *) algebras into a single finitely axiomatized variety (B R <>) resembling an R-module with ``scalar'' multiplication <>. The basic result is that * is reflexive transitive closure, contrary to the intuition that this concept should require quantifiers for its definition. Using this result we give several examples of dynamic algebras arising naturally in connection with additive functions, binary relations, state trajectories, languages, and flowcharts. The main result is that free dynamic algebras are residually finite (i.e. factor as a subdirect product of finite dynamic algebras), important because finite separable dynamic algebras are isomorphic to Kripke structures. Applications include a new completeness proof for the Segerberg axiomatization of propositional dynamic logic, and yet another notion of regular algebra. algecon.tex @InProceedings( Pr92a, Author="Pratt, V.R.", Title="Arithmetic + Logic + Geometry = Concurrency", Booktitle="Proc. First Latin American Symposium on Theoretical Informatics, LNCS 583", Pages="430-447", Publisher="Springer-Verlag", Address="Sao Paulo, Brazil", Month=Apr, Year=1992) We relate the arithmetic of concurrent schedules to the higher-dimensional cellular geometry of concurrent automata using the logic of their Birkhoff-Stone duality. This collects and unifies ideas from several of the author's previous papers. esrs.tex Event Spaces and Related Structures V.R. Pratt Manuscript, Stanford, 1992 This paper compares event spaces and their dual state spaces to some related structures. We emphasize their closest relative, event structures, but also briefly consider coherence spaces and CPO's. The most significant contribution is the application of partial partitions to the elementary description of Winskel's synchronous composition, but the remarks on the advantages of state spaces over CPO's, in particular Scott domains, for modeling fairness may also prove of interest. crewthes.tex @PhDThesis( Cre91, Author="Roger Crew", Title="Metric Process Models", School="Stanford University", Month=Dec, Year=1991) Among the various formal models proposed to provide semantics for concurrency constructs in programming languages, partial orders have the advantages of conceptual simplicity, mathematical tractability, and economy of expression. We first observe that the theory of enriched categories supplies a natural abstraction of the notion of partial order, the D-schedule. Varying the choice of temporal domain D allows for other forms of temporal constraint beyond that available from simple ordering. For example, having the constraints on inter-event delays be numeric bounds produces a generalized metric-space structure suitable for the discussion of real-time computation. We then construct an algebra of processes parametrized by notion of time. Here a process is a structure based on schedules that also incorporates nondeterminism. Since the model is category-based, we can define operations on D-schedules and processes via universal constructions that depend little on the choice of D. Also, given a suitable choice of process structure and process morphism, the constructions used for process operations and schedule operations are remarkably similar. atch.tex Interleaving Semantics and Action Refinement with Atomic Choice Rob van Glabbeek and Ursula Goltz To appear as Arbeitspapiere der GMD 594, Sankt Augustin, November 1991. We investigate how to restrict the concept of action refinement such that established interleaving equivalences for concurrent systems are preserved under these restricted refinements. We show that interleaving bisimulation is preserved under refinement if we do not allow to refine action occurrences deciding choices and action occurrences involved in autoconcurrency. On the other hand, interleaving trace equivalence is still not preserved under these restricted refinements. casthes.tex @PhDThesis( Cas91, Author="Ross Casley", Title="On the Specification of Concurrent Systems", School="Stanford University", Month=Jan, Year=1991) In models of concurrent processes constraints on the order of events are often represented by partial orders, and schedules of events are then defined using an algebra of standard operations such as sequential and parallel composition. In this dissertation the notion of partial order is replaced by that of a set with a metric which takes values in a given ordered monoid. Partial orders are the simple case of a monoid whose two elements represent the presence or absence of a constraint. An ordered monoid can be seen as a monoidal category, and schedules based on it are categories enriched in the monoid. Algebraic operations on schedules can then be defined as constructions in the category of schedules. These definitions rely on certain properties of a category of schedules, such as closure and completeness. To simplify proofs of these properties, two constructions are defined. The first creates a category of unlabeled schedules from a system of constraints. The second adds labels to unlabeled schedules. Many categories of interest can be constructed from simple categories using these two methods. The main results of the dissertation derive the required properties of categories so constructed from similar, more easily verified properties of the base categories. Several notions of timing constraint can be viewed in a uniform way in this framework. An example is the Gaifman-Pratt system, essentially the partial order model with additional specification as to whether two events may occur simultaneously. It corresponds to a monoid whose three elements represent strict precedence, lax precedence (simultaneity is permitted), and absence of constraint. Real-valued timing constraints correspond to the additive monoid of the real numbers. es.tex @InProceedings( Pr91b, Author="Pratt, V.R.", Title="Event Spaces and Their Linear Logic", Booktitle="Proc. Second International Conference on Algebraic Methodology and Software Technology", Address="Iowa City", Month=May, Year=1991) Boolean logic treats disjunction and conjunction symmetrically and algebraically. The corresponding operations for computation are respectively nondeterminism (choice) and concurrency. Petri nets treat these symmetrically but not algebraically, while event structures treat them algebraically but not symmetrically. Here we achieve both via the notion of an event space as a poset with all nonempty joins representing concurrence and a top representing the unreachable event. The symmetry is with the dual notion of state space, a poset with all nonempty meets representing choice and a bottom representing the start state. The algebra is that of a parallel programming language expanded to the language of full linear logic, Girard's axiomatization of which is satisfied by the event space interpretation of this language. Event spaces resemble finite-dimensional vector spaces in distinguishing tensor product from direct product and in being isomorphic to their double dual, but differ from them in distinguishing direct product from direct sum and tensor product from tensor sum. cg.tex @InProceedings( Pr91a, Author="Pratt, V.R.", Title="Modeling Concurrency with Geometry", Booktitle="Proc. 18th Ann. ACM Symposium on Principles of Programming Languages", Pages="311-322", Month=Jan, Year=1991) Branching time and causality find their respective homes in the Birkhoff-dual models of automata and schedules. This creates a puzzle: if the duality is supposed to make the models completely equivalent then why does each phenomenon have a preferred side? We identify dimension as the culprit: 1-dimensional automata are skeletons permitting only interleaving concurrency, true n-fold concurrency resides in transitions of dimension n. The Birkhoff dual of a poset then becomes a simply-connected space. We distinguish Birkhoff duality from Stone duality and treat the former in detail from a concurrency perspective. We introduce true nondeterminism and define it as monoidal homotopy; from this perspective nondeterminism in ordinary automata arises from forking and joining creating nontrivial homotopy. We propose a formal definition of higher dimensional automaton as an n-complex or n-category, whose two essential axioms are associativity of concatenation within dimension and an interchange principle between dimensions. jelia.tex @InProceedings( Pr90b, Author="Pratt, V.R.", Title="Action Logic and Pure Induction", Booktitle="Logics in AI: European Workshop JELIA '90, LNCS 478", Editor="J. van Eijck", Publisher="Springer-Verlag", Pages="97-120", Address="Amsterdam, NL", Month=Sep, Year=1990) In Floyd-Hoare logic programs are dynamic while assertions are static (hold at states). In action logic the two notions become one, with programs viewed as on-the-fly assertions whose truth is evaluated along intervals instead of at states. Action logic is an equational theory ACT conservatively extending the equational theory REG of regular expressions with operations preimplication a -> b (HAD a THEN b) and postimplication b <- a (b IF-EVER a). Unlike REG, ACT is finitely based, makes a* reflexive transitive closure, and has an equivalent Hilbert system. The crucial axiom is that of pure induction, (a -> a)* = a -> a. man.tex Temporal Structures R. Casley, R. Crew, J. Meseguer, V. Pratt To appear in Mathematical Structures in Computer Science, 1:2. Proceedings version in Category Theory and Computer Science, LNCS 389, Manchester, 1989. Formerly called "Dynamic Types." We combine the principles of the Floyd-Warshall-Kleene algorithm, enriched categories, and Birkhoff arithmetic, to yield a useful class of algebras of transitive vertex-labeled spaces. The motivating application is a uniform theory of abstract or parametrized time in which to any given notion of time there corresponds an algebra of concurrent behaviors and their operations, always the same operations but interpreted automatically and appropriately for that notion of time. An interesting side application is a language for succinctly naming a wide range of datatypes. pp2.tex Teams Can See Pomsets G. Plotkin and V. Pratt Draft in preparation Strings may serve as both specifications and observations of behavior. However partial strings or pomsets, superior to strings in certain respects for the representation of concurrent behavior, are provably unobservable and hence apparently suitable only for specifying behavior. The proof however tacitly assumes that observers are isolated individuals. We show that observations by a cooperating team of sequential observers agreeing on *what* happened but not *when* can distinguish all pomsets. The resolving power of a finite team increases strictly with its size k, permitting it to distinguish all pomsets of dimension (not width) k but not all of k+1. These results extend to observation of augment closed processes. As expected we depend on the now standard technique of refinement of atomic events to complex events; what is not expected is that their complexity need be only that of nondeterminism, in that we refine one atomic event to a set of alternative atomic events, not to a set of sequences. am4.tex @InProceedings( Pr89a, Author="Pratt, V.R.", Title="Enriched Categories and the {Floyd-Warshall} Connection", Booktitle="Proc. First International Conference on Algebraic Methodology and Software Technology", Pages="177-180", Address="Iowa City", Month=May, Year=1989) We give a correspondence between enriched categories and the Gauss-Kleene-Floyd-Warshall connection familiar to computer scientists. This correspondence shows this generalization of categories to be a close cousin to the generalization of transitive closure algorithms. Via this connection we may bring categorical and 2-categorical constructions into an active but algebraically impoverished arena presently served only by semiring constructions. We illustrate these techniques by applying them to Birkoff's poset arithmetic, interpretable as an algebra of ``true concurrency.'' iowatr.tex @InProceedings( Pr90a, Author="Pratt, V.R.", Title="Dynamic Algebras as a Well-behaved Fragment of Relation Algebras", Booktitle="Algebraic Logic and Universal Algebra in Computer Science, LNCS 425", Editors="C.H. Bergman, R.D. Maddux, D.L. Pigozzi", Address="Ames, Iowa, June 1988", Publisher="Springer-Verlag", Year=1990) The varieties RA of relation algebras and DA of dynamic algebras are similar with regard to definitional capacity, admitting essentially the same equational definitions of converse and star. They differ with regard to completeness and decidability. The RA definitions that are incomplete with respect to representable relation algebras, when expressed in their DA form are complete with respect to representable dynamic algebras. Moreover, whereas the theory of RA is undecidable, that of DA is decidable in exponential time. These results follow from representability of the free intensional dynamic algebras. ijpp.tex @Article( Pr86, Author="Pratt, V.R.", Title="Modeling Concurrency with Partial Orders", Journal="Int. J. of Parallel Programming", Volume=15, Number=1, Pages="33-71", Month=Feb, Year=1986) Concurrency has been expressed variously in terms of formal languages (typically via the shuffle operator), partial orders, and temporal logic, inter alia. In this paper we extract from these three approaches a single hybrid approach having a rich language that mixes algebra and logic and having a natural class of models of concurrent processes. The heart of the approach is a notion of partial string derived from the view of a string as a linearly ordered multiset by relaxing the linearity constraint, thereby permitting partially ordered multisets or pomsets. Just as sets of strings form languages, so do sets of pomsets form processes. We introduce a number of operations useful for specifying concurrent processes and demonstrate their utility on some basic examples. Although none of the operations is particularly oriented to nets it is nevertheless possible to use them to express processes constructed as a net of subprocesses, and more generally as a system consisting of components. The general benefits of the approach are that it is conceptually straightforward, involves fewer artificial constructs than many competing models of concurrency, yet is applicable to a considerably wider range of types of systems, including systems with buses and ethernets, analog systems, and real-time systems.